1. Technical Field
The present invention relates in general to testing and verification, and in particular to verification of digital designs. Still more particularly, the present invention relates to a system, method and computer program product for verification of digital designs, which includes verifying conformance of a design to a desired property.
2. Description of the Related Art
With the increasing penetration of processor-based systems into every facet of human activity, demands have increased on the processor and application-specific integrated circuit (ASIC) development and production community to produce systems that are free from design flaws. Circuit products, including microprocessors, digital signal and other special-purpose processors, and ASICs, have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of error-free and flaw-free design. Whether the impact of errors in design would be measured in human lives or in mere dollars and cents, consumers of circuit design would be measured in human lives or in mere dollars and cents, consumers of circuit products have lost tolerance for results polluted by design errors. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable circuit results has risen to a mission-critical concern.
In response to the increasing need for reliable, error-free designs, the processor and ASIC design and development community has developed rigorous, if incredibly expensive, methods for testing and verification. Functional hardware verification has been a traditional method for verifying such complex designs as processor chips. Because the functional hardware verification time for a design grows in relation to the number of logic elements, functional hardware verification of complex systems is one of the most time-consuming computing tasks today. It is therefore important to use functional hardware verification cycles effectively, with the aim that few bugs escape and development time is reduced.
As mentioned above, functional hardware verification is a computationally expensive process; for sequential designs, functional hardware verification is a PSPACE-complete problem (by algorithmic complexity analysis) and hence generally requires resources which are exponential with respect to the size of the design under verification. Many prior art function hardware verification proof algorithms rely upon reachability analysis, which requires enumerating the reachable states of the design under test to assess whether the design conforms to its specification, which unfortunately is a size-limited process.
Reachability analysis is a powerful verification framework; it is able to identify whether a design satisfies its specification (i.e., if all reachable states of a design satisfy the property being verified, then a correctness proof has been completed) and also whether the design does not satisfy its specification (if any of the reachable states does not satisfy the property being verified). Reachability algorithms operate by assigning R_0 to be the set of predefined initial states of the design under verification, then assign R_{i+1}(for increasing i) to be the set of all states which may be reached in one design transition from R_i. Eventually, R_{i+1} will be a subset of all the previous states encountered in R_0 . . . R_i, after which this process will terminate; this final set of reachable states is referred to as R. To partially alleviate some of the computational overhead of the expensive process of computing the exact set of reachable states, there have been numerous proposals to “overapproximate” the set of reachable states. For example, some authors have proposed using “inductive” methods. The drawback of prior art overapproximation methods is that they are often inconclusive, resulting in “spurious failures” due to their overapproximate nature.
Despite decades of research in improving the performance of reachability analysis, such techniques are still limited in application to designs with several hundreds of state elements or less and are also hindered by other design size metrics. Because of the size limitations of reachability analysis, there has been some research in ways to overapproximate the reachable state set to enable computational shortcuts. For example, inductive proofs begin with R_0 being all states which do not themselves violate a property (after guaranteeing that the actual initial states of the design are a subset of this overapproximated R_0), and compute an overapproximated set R′ starting from this overapproximated initial state set. The benefits of this approach include a substantial decrease in the number of steps needed to complete the analysis. The main drawback of this inductive approach is that it often renders an inconclusive result. In particular, if the overapproximated set R′ contains some states S′ which violate the property being verified, one cannot immediately discern if this violation is only due to the overapproximation of the initial state set (i.e., S′ is a subset of R′-R), or if S′ contains some truly reachable states in R. The former case is a spurious failure of the property being verified. What is needed is a more efficient method for verifying digital designs utilizing a functional hardware verification model, and more particularly, for verifying digital designs utilizing an enhanced overapproximation method.